\section{Transformaci\'on de estados del auxiliar usuariosDeLasTrivias}

\subsection{Transformaci\'on de estados del cuerpo principal}

\begin{lstlisting}
int TelCO:: usuariosDeLasTrivias(const Gateway& g) const{
  int i=0;
  int acum=0;
  Lista<Trivia> trivias = g.trivias();
\end{lstlisting}
$//Pc: Vale\ i == 0 \ylogico acum == 0 \ylogico trivias == trivias(g) $ 
\begin{lstlisting}
  while (i < usuarios(this).longitud()){
\end{lstlisting}
$//Vale\ invariante\ I: 0 \leq i \leq \longitud{usuarios(this)} \ylogico \\
//acum == \longitud{ \comp{j}{j \selec [0..i), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} } \\
//Funcion\ variante\ V: \longitud{usuarios(this)} - i$
\begin{lstlisting}
        if( estaEnAlgunaTrivia(usuarios().iesimo(i), trivias) )
            acum++;
        i++;
    }
\end{lstlisting}
$//Qc: Vale\ acum == \longitud{ \comp{j}{j \selec [0..\longitud(usuarios(this))), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} }$ 
\begin{lstlisting}
  return acum;
\end{lstlisting}
\begin{lstlisting}
}
\end{lstlisting}


\subsection{Transformaci\'on de estados del cuerpo del ciclo}
\begin{lstlisting}
while (i < usuarios(this).longitud()){
\end{lstlisting}
$//C1: Vale\ I \ylogico B$
\begin{lstlisting}
  if( estaEnAlgunaTrivia(usuarios().iesimo(i), trivias) ){
\end{lstlisting}
	$//T1: Vale\ estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@C1 \ylogico acum == acum@C1 $
	\begin{lstlisting}
    acum++;
    \end{lstlisting}
    $//T2: Vale\ estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@T1 \ylogico acum == acum@T1 + 1  $
\begin{lstlisting}
  }
\end{lstlisting}
$//C2: (estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@T1 \ylogico acum == acum@T1 + 1) \ologico \\
(\neg estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@C1 \ylogico acum == acum@C1)$
    
\begin{lstlisting}
i++;
\end{lstlisting}

$//C3: i == i@C2+1 \ylogico acum == acum@C2 $
  
\begin{lstlisting}
}
\end{lstlisting}


\section{Demostraci\'on del cuerpo del problema}

Suponiendo que el ciclo es correcto respecto de su especificaci\'on, queremos ver que vale la poscondici\'on del problema.

\begin{problema}{usuariosDeLasTrivias}{this:TelCO, g:Gateway}{\ent}{
    \asegura{result == cuantosJueganAlgunaTrivia(this, g)}}
\end{problema}

\begin{aux}{cuantosJueganAlgunaTrivia}{t:TelCO,g:Gateway}{\ent}{
   \longitud{\comp{u}{u \selec usuarios(t),(\exists x \selec trivias(g))u \in participantes(x)}}}
\end{aux}
\medskip
$//Qc: Vale\ acum == \longitud{ \comp{j}{j \selec [0..\longitud(usuarios(this))), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} }$ 
\begin{lstlisting}
    return acum;
}
\end{lstlisting}

La demostraci\'on es bastante directa, solo hace falta usar la especificaci\'on del auxiliar estaEnAlgunaTriviaAux.

\begin{aux}{estaEnAlgunaTriviaAux}{t:TelCO, u:Usuario, ts:[Trivias]}{Bool}{
    u \in (concat (\comp{participantes(ts_p)}{p \selec [0..\longitud{ts})})}
\end{aux}

Queremos ver que
$\longitud{ \comp{j}{j \selec [0..\longitud(usuarios(this))), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} } \\
== \longitud{\comp{u}{u \selec usuarios(this),(\exists x \selec trivias(g))u \in participantes(x)}}$\\

Por la definici\'on de estaEnAlgunaTriviaAux, vemos que es l\'ogicamente equivalente a decir que existe una trivia tal que el usuario pertenece a sus participantes.\\

Entonces, cambiando los selectores de \'indices ($j$) por selectores directos de elementos ($u$), vemos que las expresiones de ambas listas por compresi\'on son equivalentes. \\
Reemplazando por la variable $acum$ (usando que vale $Qc$: \\
$acum == \longitud{ \comp{u}{u \selec [0..\longitud(usuarios(this))), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} }$ 

Luego, probamos que la variable $acum$ cumple la poscondici\'on del problema.\\


\section{Demostraci\'on del cuerpo del ciclo}

\subsection{$Pc \implica I$}
Supongamos que vale Pc. Queremos ver que vale I.\\
De Pc sabemos que $acum == 0$ y que $i == 0$, del invariante sabemos que:\\
\\
(1) $0 \leq i \leq \longitud{usuarios(this)}$\\
\\
(2) $acum == \longitud{ \comp{j}{j \selec [0..i), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} }$\\
\\
- Como $i==0$ por Pc entonces (1) es valido, porque $0 \leq \longitud{usuarios(this)}$.\\
- Sabemos que con $i==0$, $[0..i) == []$, por propiedades de listas. \\
Entonces sabemos que siendo el selector vacio de la lista por comprension de (2), $acum==\longitud{[]}==0$.\\
Que es lo que queriamos ver.

\subsection{La funci\'on variante es estrictamente decreciente}
$Funcion\ variante\ V: \longitud{usuarios(this)} - i$ \\
Queremos ver que $ V@C3 < V@C1 $. Sabemos que la longitud de los usuarios no se modifica y que $ i@C3 == i@C1 + 1 $ por la transformaci\'on de estados.
Luego, $ V@C1 == \longitud{usuarios(this)} - i@C1 > \longitud{usuarios(this)} - (i@C1 + 1) == \longitud{usuarios(this)} - i@C3 == V@C3 $.

\subsection{$V < 0 \implica \neg B$}
$Funcion\ variante\ V: \longitud{usuarios(this)} - i \\
B: i < \longitud{usuarios(this)} $ \\
Queremos ver que si $ V < 0 $ el ciclo termina, es decir que vale $ \neg B $. Sabemos que: \\
$ V < 0 \implica \longitud{usuarios(this)} - i < 0 \implica i > \longitud{usuarios(this)} \implica \neg B $

\subsection{$I \ylogico \neg B \implica Qc $}
$I: 0 \leq i \leq \longitud{usuarios(this)} \ylogico \\
acum == \longitud{ \comp{j}{j \selec [0..i), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} }$
$B: i < \longitud{usuarios(this)} \implica \neg B: i \geq \longitud{usuarios(this)}$

Por el termino de intervalo de I, y por la negacion de la guarda B, nos queda que:

$0 \leq i \leq \longitud{usuarios(this)} \ylogico i \geq \longitud{usuarios(this)}
\implica i == \longitud{usuarios(this)}$ que lo llamamos (1)

Reemplazando (1) en la igualdad del acum nos queda \\
$\longitud{ \comp{j}{j \selec [0..\longitud{usuarios(this)}), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} } \implica Qc$ 

\subsection{El cuerpo del ciclo preserva el invariante}
Volvamos a la trasnformaci\'on de estados y sigamos las implicaciones.

\begin{lstlisting}
while (i < usuarios(this).longitud()){
\end{lstlisting}
$//C1: Vale\ I \ylogico B \\
//Implica: 0 \leq i < \longitud{usuarios(this)} \ylogico \\
acum == \longitud{ \comp{j}{j \selec [0..i), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} }$
\begin{lstlisting}
  if( estaEnAlgunaTrivia(usuarios().iesimo(i), trivias) ){
\end{lstlisting}
	$//T1: Vale\ estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@C1 \ylogico acum == acum@C1 $
	\begin{lstlisting}
    acum++;
    \end{lstlisting}
    $//T2: Vale\ estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@T1 \ylogico acum == acum@T1 + 1 $\\
    $//Implica: estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@C1 \ylogico acum == acum@C1 + 1 $
\begin{lstlisting}
  }
\end{lstlisting}
$//C2: (estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@T1 \ylogico acum == acum@T1 + 1) \ologico \\
(\neg estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@C1 \ylogico acum == acum@C1)$\\
$//Implica: (estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@C1 \ylogico acum == acum@C1 + 1) \ologico \\
(\neg estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@C1 \ylogico acum == acum@C1)$

Dado que si la guarda del if es verdadera, se suma uno a $acum$, y si no lo es no se ejecuta ninguna instrucci\'on.
    
\begin{lstlisting}
  i++;
\end{lstlisting}

$//C3: i == i@C2+1 \ylogico acum == acum@C2 $\\
$//Implica: i == i@C1 + 1 \ylogico ((estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico acum == acum@C1 + 1) \ologico \\
(\neg estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico acum == acum@C1))$


\begin{lstlisting}
}
\end{lstlisting}

Queremos probar que el invariante vale en C3 suponiendo que val\'ia en C1, y usando las implicaciones de la transformaci\'on de estados.
$I: 0 \leq i \leq longitud{usuarios(this)} (1) \ylogico \\
acum == \longitud{ \comp{j}{j \selec [0..i), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} } (2)$

Probaremos por separado (1) y (2). \\
(1): Sabemos que $i@C3 == i@C1 + 1$. Como para entrar al ciclo hac\'ia falta que valiera B, eso quiere decir que \\
$i@C1 < \longitud{usuarios(this}$.
Como tanto $i$ como $\longitud{usuarios(this)}$ son enteras, podemos concluir que en C3 $i \leq \longitud{usuarios(this)}$.
Como el invariante val\'ia en C1, sabemos tambi\'en que $0 \leq i@C1 \implica 0 \leq i@1 + 1$.\\

(2): Por $C2$ sabemos que vale\\
$(estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@C1 \ylogico acum == acum@C1 + 1) \ologico \\
(\neg estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias) \ylogico i == i@C1 \ylogico acum == acum@C1)$
y ademas sabemos que el invariante vale en $C1$, es decir que \\
$acum@C1 == \longitud{ \comp{j}{j \selec [0..i), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} }$

Tambi\'en sabemos que le agregamos un elemento o no dependiendo de estaEnAlgunaTriviaAux. Es decir, que la lista mantiene su forma
si aumentamos el rango del selector incluyendo a $j == i@C2$, porque en caso de no haberlo agregado la condici\'on de la lista por
compresi\'on se encarga de filtrarlo.

Usando esto, podemos asegurar que \\
$acum@C2 == \longitud{ \comp{j}{j \selec [0..i], estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} } $ \\
dado que suma uno si la condici\'on de la lista devolvi\'o $True$.

En C3, $i == i@C2 + 1$, por lo tanto la variable quedar\'ia: \\
$acum == \longitud{ \comp{j}{j \selec [0..i), estaEnAlgunaTriviaAux(this, usuarios(this)_j, trivias)} } $\\
por propiedad de listas ($[0..i] == [0..i+1)$). Y esta expresi\'on es exactamente (2) $\square$.